/LMAR=0/XLINE=3/FONT#0=BAXL30[FNT,CLT]/FONT#1=BAXM30/FONT#2=BAXB30[FNT,CLT]/FONT#5=GACS25/FONT#3=SUB/FONT#4=SUP/FONT#7=SYMB30[FNT,CLT]

␈↓ ↓H␈↓␈↓ ∧+COMPUTER SCIENCE DEPARTMENT
␈↓ ↓H␈↓␈↓ ¬πSTANFORD UNIVERSITY
␈↓ ↓H␈↓CS206  ␈↓ βiRECURSIVE PROGRAMMING AND PROVING ␈↓ 
0FALL 1979
␈↓ ↓H␈↓␈↓ ¬DPROBLEM SET  4
␈↓ ↓H␈↓␈↓ ¬pDue  Nov. 29

␈↓ ↓H␈↓1. program transformer

␈↓ ↓H␈↓2. iterative program→elephant→proof

␈↓ ↓H␈↓3. more to do with λ
␈↓ ↓H␈↓        Interctive top level
␈↓ ↓H␈↓        Deduction to which steps can be added.
␈↓ ↓H␈↓        Use Errset or catch/throw for errors
␈↓ ↓H␈↓        Use rplacs for modifications when safe?
␈↓ ↓H␈↓        Show how numbers, successor, conditionals, true, false, pairs
␈↓ ↓H␈↓                can be represented as λ's give a few interesting derivations
␈↓ ↓H␈↓                to be tried.